/*!
 *\mainpage IEGen C++ Rewrite
 *\authors Alan LaMielle
 *\authors Michelle Strout
 *\authors Ian Craig
 *\authors Nicholas Jeanette
 *\date Date Started: 5/17/10
 *\date Date Last Updated: 9/13/10
 *
 *\section Intro
 *  Currently IEGenC is just a library with data structures and routines that
 *  can represent, parse, and visit integer tuple sets and relations with affine
 *  constraints and uninterpreted function symbol equality constraints. See
 *  src/parser/pres_parser_test.cc for examples of strings that can be parsed
 *  into an abstract syntax tree (Note that PresSet and PresRelation are AST
 *  node types).
 *
 *  The run_tests.cc driver will execute all tests identified with the TEST
 *  macro. In each of the src/ subdirectories, the *_test.cc files define
 *  regression tests.
 *
 *  The demo_driver binary will execute tests that you input yourself and will
 *  return the interpreted version of the input along with a dotty file to the
 *  standard out.
 *
 *  We are currently working on translating the AST representation of sets and
 *  relations into the SparseConstraints representation. The SparseConstraints
 *  representation is better organized for enabling operations over sets and/or
 *  relations.
 *
 *

 *\section README
 *\verbinclude README

 *\section COPYING
 *\verbinclude COPYING
 */

#include <iostream>
#include <fstream>
#include <iegenlib/iegenlib.h>

#include <assert.h>

#include <isl/ctx.h>
#include <isl/set.h>
#include <isl/map.h>
#include <isl/printer.h>

using iegenlib::ParseException;
using iegenlib::UFCALL;
using iegenlib::SymType;
using iegenlib::Set;
using iegenlib::Relation;

#define SET_RELATION_DOT_FILE_NAME "set_relation.dot"
#define AST_DOT_FILE_NAME "ast.dot"

int main(int ac, char **av)
{
  string set_relation_str;

  Set *set, *set2;
  isl_basic_set *isl_set;
  Relation *relation, *relation2;
  isl_basic_map *isl_map;

  ofstream dot_file;

  isl_ctx *ctx=NULL;
  isl_printer *printer=NULL;

  //Allocate an ISL context and printer
  ctx=isl_ctx_alloc();
  assert(ctx);
  printer=isl_printer_to_str(ctx);
  assert(printer);

  //Print a startup message
  std::cout<<endl;
  std::cout<<"==============================================================="<<endl;
  std::cout<<"This is a demo driver for IEGen."<<endl<<endl;
  std::cout<<"Please enter a set, relation, or operation string.  Some examples of sets are:";
  std::cout<<endl<<endl;
  std::cout<<"{[a]}  {[a]: a=10}  {[a,b]}  {[a,b]: a=f(b)}"<<endl<<endl;
  std::cout<<"and some examples of relations are:"<<endl<<endl;
  std::cout<<"{[a]->[b]}  {[a]->[b]: a=b}"<<endl;
  std::cout<<"{[a,b]->[c]: 0<=a and a<10 and b=10 and b=c}"<<endl;
  std::cout<<"{[a]->[b,c]: 0<=a and a<10 and b=c}"<<endl<<endl;
  std::cout<<"and some examples of operations are:"<<endl<<endl;
  std::cout<<"Union: {[i,j]: 0<=i and i<n and 5<=j and j<m} Union {[i,j]: 0<=i and i<n and m+5<=j and j<m+10}"<<endl;
  std::cout<<"Apply: {[i,j]->[ip,jp]:ip=f(i) and jp=j} Apply {[i,j]: 0<=i and i<n and 5<=j and j<m}"<<endl;
  std::cout<<"Compose: {[i,j]->[ip,jp]: ip=f(i) and jp=2j} Compose {[q,r]->[i,j]: i=q and j=r}"<<endl;
  std::cout<<"Inverse: {[i,j]->[ip,jp]: ip=f(i) and jp=2j} Inverse"<<endl<<endl;
  std::cout<<"Enter an empty string or Ctrl-D to quit..."<<endl<<endl;
  std::cout<<"==============================================================="<<endl;

  //Read a set/relation string
  std::cout<<endl;
  std::cout<<"-------------"<<endl;
  std::cout<<"Enter Set/Relation> ";
  getline(std::cin,set_relation_str);

  while(""!=set_relation_str)
  {
    size_t opLoc = string::npos; //string::npos = -1
    //Print the string we received as input
    std::cout<<"read: "<<set_relation_str<<endl;

    // Determine if the given string is a set or relation
    // by searching for the '->' sequence of characters
    try{
      if((opLoc = set_relation_str.find("Union"))!=string::npos)
      {
        string opLeft = set_relation_str.substr(0, opLoc);
        string opRight = set_relation_str.substr(opLoc+5,set_relation_str.size()-(opLoc+4));
        if(opLeft.find("->[") == string::npos){
          set = new Set(opLeft);
          if(opRight.find("->[") == string::npos){
            set2 = new Set(opRight);
            string isl = set->Union(*set2).get_isl();
            std::cout<<"union->get_isl(): "<<isl<<endl;
            delete set2;
          }else{
            delete set;
            throw ParseException("Union requires two elements of the same type!\nUsage: [set/relation] union [set/relation]");
          }
          delete set;
        }else{
          relation = new Relation(opLeft);
          if(opRight.find("->[") != string::npos){
            relation2 = new Relation(opRight);
            string isl = relation->Union(*relation2).get_isl();
            std::cout<<"union->get_isl(): "<<isl<<endl;
            delete relation2;
          }else{
            delete relation;
            throw ParseException("Union requires two elements of the same type!\nUsage: [set/relation] union [set/relation]");
          }
          delete relation;
        }
      }
      else if((opLoc = set_relation_str.find("Apply")) != string::npos)
      {
        string opLeft = set_relation_str.substr(0, opLoc);
        string opRight = set_relation_str.substr(opLoc+5,set_relation_str.size()-(opLoc+4));
        if(opLeft.find("->[") != string::npos){
          relation2 = new Relation(opLeft);
          if(opRight.find("->[") == string::npos){
            set = new Set(opRight);
            string isl = relation2->Apply(*set).get_isl();
            std::cout<<"apply->get_isl(): "<<isl<<endl;
            delete set;
          }else{
            delete relation2;
            throw ParseException("Apply requires one element of each same type!\nUsage: [relation] apply [set]");
          }
          delete relation2;
        }
      }
      else if((opLoc = set_relation_str.find("Compose")) != string::npos)
      {
        string opLeft = set_relation_str.substr(0, opLoc);
        string opRight = set_relation_str.substr(opLoc+7,set_relation_str.size()-(opLoc+6));
        if(opLeft.find("->[") != string::npos){
          relation = new Relation(opLeft);
          if(opRight.find("->[") != string::npos){
            relation2 = new Relation(opRight);
            string isl = relation->Compose(*relation2).get_isl();
            std::cout<<"compose->get_isl(): "<<isl<<endl;
            delete relation2;
          }else{
            delete relation;
            throw ParseException("Compose requires two relations!\nUsage: [relation] compose [relation]");
          }
          delete relation;
        }else{
          throw ParseException("Compose requires two relations!\nUsage: [relation] compose [relation]");
        }
      }
      else if((opLoc = set_relation_str.find("Inverse")) != string::npos)
      {
        string opLeft = set_relation_str.substr(0, opLoc);
        if(opLeft.find("->[") != string::npos){
          relation = new Relation(opLeft);
          string isl = relation->Inverse().get_isl();
          std::cout<<"inverse->get_isl(): "<<isl<<endl;
          delete relation;
        }else{
          throw ParseException("Inverse requires one relation!\nUsage: [relation] inverse");
        }
      }
      else if(set_relation_str.find("->[")==string::npos)
      {
        //Create a set from the given set string
        set=new Set(set_relation_str);

        //Print the result of the get_isl() method of the set
        std::cout<<"set->get_isl(): "<<set->get_isl()<<endl;

        //Print the result of the get_dot() method of the set
        //to the file SET_RELATION_DOT_FILE_NAME
        dot_file.open(SET_RELATION_DOT_FILE_NAME);
        std::cout<<"Writing output of set->get_dot() to file '"
            <<SET_RELATION_DOT_FILE_NAME;
        std::cout<<"'..."<<endl;
        dot_file<<set->get_dot();
        dot_file.close();

        //Print the result of the getAST() method of the set
        //to the file AST_DOT_FILE_NAME
        dot_file.open(AST_DOT_FILE_NAME);
        std::cout<<"Writing output of set->getAST() to file '"<<AST_DOT_FILE_NAME;
        std::cout<<"'..."<<endl;
        dot_file<<set->getAST();
        dot_file.close();

        //If there are no functions in the given set...
        map<SymType,int> totals=set->getTotals();
        if(0==totals[UFCALL])
        {
           //Create an ISL set from the given set string
           /*isl_set=isl_basic_set_read_from_str(ctx,set_relation_str.c_str(),-1);
           assert(isl_set);
           isl_printer_print_basic_set(printer,isl_set);
           char *isl_set_str=isl_printer_get_str(printer);
           std::cout<<"ISL string of set: "<<isl_set_str<<endl;
           free(isl_set_str);
           isl_printer_flush(printer);
           isl_basic_set_free(isl_set);
           isl_set=NULL;*/
        }

        //Delete the allocated set
        delete set;
      }
      else
      {
        //Create a relation from the given relation string
        relation=new Relation(set_relation_str);

        //Print the result of the get_isl() method of the relation
        std::cout<<"relation->get_isl(): "<<relation->get_isl()<<endl;

        //Print the result of the get_dot() method of the relation
        //to the file SET_RELATION_DOT_FILE_NAME
        dot_file.open(SET_RELATION_DOT_FILE_NAME);
        std::cout<<"Writing output of relation->get_dot() to file '"
            <<SET_RELATION_DOT_FILE_NAME;
        std::cout<<"'..."<<endl;
        dot_file<<relation->get_dot();
        dot_file.close();

        //Print the result of the getAST() method of the relation
        //to the file AST_DOT_FILE_NAME
        dot_file.open(AST_DOT_FILE_NAME);
        std::cout<<"Writing output of relation->getAST() to file '"<<AST_DOT_FILE_NAME;
        std::cout<<"'..."<<endl;
        dot_file<<relation->getAST();
        dot_file.close();

        //If there are no functions in the given relation...
        map<SymType,int> totals=relation->getTotals();
        if(0==totals[UFCALL])
        {
           //Create an ISL map from the given relation string
           /*isl_map=isl_basic_map_read_from_str(ctx,set_relation_str.c_str(),-1);
           assert(isl_map);
           isl_printer_print_basic_map(printer,isl_map);
           std::cout<<"ISL string of relation: "<<isl_printer_get_str(printer)<<endl;
           isl_printer_flush(printer);
           isl_basic_map_free(isl_map);
           isl_map=NULL;*/
        }

        //Delete the allocated relation
        delete relation;
      }
    }catch(ParseException s){
       std::cerr << s.what() << endl;
    }
    //Get the next set/relation string
    std::cout<<endl<<"-------------"<<endl;
    std::cout<<"Enter Set/Relation> ";
    getline(std::cin,set_relation_str);
  }

  //Free the ISL structures
  isl_printer_free(printer);
  printer=NULL;
  isl_ctx_free(ctx);
  ctx=NULL;

  std::cout<<endl<<"Exiting..."<<endl;

  return 0;
}
